\begin{tabbing}
$\forall$${\it es}$:ES, $L$:(Id List).
\\[0ex]fischer($L$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$, ${\it e'}$:E.\+
\\[0ex]fEvent($e$)
\\[0ex]$\Rightarrow$ fEvent(${\it e'}$)
\\[0ex]$\Rightarrow$ (rank($e$) = rank(${\it e'}$) $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$))
\\[0ex]$\Rightarrow$ (loc($e$) = loc(${\it e'}$) $\in$ Id)
\\[0ex]$\Rightarrow$ ($e$ = ${\it e'}$))
\-
\end{tabbing}